Inference at * 
Iof proof for Lemma member nth tl:


  T:Type, n:, x:T, L:(T List). (x  nth_tl(n;L))  (x  L) 

latex

 by InductionOnNat 

latex

 1: .....basecase..... NILNIL

 1: 1. T : Type
 1:   x:T, L:(T List). (x  nth_tl(0;L))  (x  L)
 2: .....upcase..... NILNIL

 2: 1. T : Type
 2: 2. n : 
 2: 3. 0 < n
 2: 4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
 2:   x:T, L:(T List). (x  nth_tl(n;L))  (x  L)
 .

Definitions	Void, a < b, n - m, n+m, -n, #$n, A, False, i  j , A  B, {x:A| B(x)} , x:A. B(x), P  Q, (x  l), type List, x:AB(x), Type, , t  T, s = t
Lemmas	ge wf, nat properties, l member wf, nat wf, nat ind tp